Programación Avanzada

1 Contenido de la clase

Aclaraciones sobre el examen (en equipos de dos) [00:00-00:52]

Antes de empezar el tema se aclara la modalidad del examen: se rinde en equipos de dos, los integrantes se ponen de acuerdo y entregan un solo examen; la aplicación es igual para los dos [00:00-00:52]. Los detalles de corrección y puntajes quedan en la parte ininteligible del audio: [parte no entendida — criterios de puntaje y condiciones mencionados].

Repaso: la resolución y la demostración automática [00:52-02:36]

Se retoma la resolución como el modelo de computación que surgió con los intentos de programación y para demostrar la validez de fórmulas [00:52-01:20]. Se recuerda el método de demostración para probar una conclusión a partir de las premisas, equivalente al modus ponens [01:20-01:52]. Al encontrar la fórmula y su negación, el sistema deduce en base a esos principios [02:21-02:36]. [parte no entendida — parte de la explicación del modelo de computación].

Ejemplo de resolución con predicados (estudia / trabaja / va al cine) [02:36-04:44]

Se aplica la resolución a cláusulas con predicados, como R(x), F(x), T(x), pensados como "estudia", "trabaja" y "va al cine" [02:36-03:08]. Para demostrar una conclusión se niega la meta, se la agrega al conjunto y se aplica la resolución cancelando los literales opuestos (¬R con R, ¬F con F, etc.) hasta la contradicción [03:08-04:44]. Así, de R(x) ∨ F(x) y ¬F(x) ∨ T(x) (o ¬F(x) → T(x)) se cancela F(x) con ¬F(x) y se concluye T(x) [02:36-04:44].

Otro ejemplo de resolución paso a paso [04:44-09:47]

Se desarrolla un segundo ejemplo en el que las cláusulas se reescriben (negando y reordenando literales) para poder aplicar la resolución [04:44-08:49]. Al cancelar literales opuestos queda el resolvente R(x), que luego se combina con ¬R(x) hasta producir la contradicción [08:49-09:47]. [parte no entendida — gran parte de este tramo; hay un corte entre 09:47 y 20:00].

Explosión combinatoria y el paso a las cláusulas de Horn [20:00-21:58]

Se retoma el inconveniente de la resolución: la explosión combinatoria. Con pocas cláusulas hay que probar muchísimas combinaciones (se mencionan conjuntos de "1, 2, 3, 4" y hasta de "100" cláusulas con muchas combinaciones), lo que lleva a "caminos sin salida" [20:00-20:58]. La solución es restringirse a un subconjunto de cláusulas para reducir la explosión [20:50-21:44]. Aunque las máquinas son rapidísimas, conviene limitar las combinaciones [21:01-21:26]; restringiéndose a esa clase de cláusulas se pudo programar el método y así nació el lenguaje de programación lógica [21:40-21:58].

Elementos del lenguaje de la lógica de primer orden [22:04-24:35]

Se repasan los elementos del lenguaje: las constantes (nombres de objetos o personas, p. ej. Juan, María) y las variables, que se escriben con letra mayúscula (X) y representan cualquier objeto o persona [22:35-23:03]. Las funciones asocian un nombre a sus argumentos constantes y devuelven un valor [23:15-23:45]. Un término es una constante, una variable o una función junto con sus argumentos [23:45-24:09]. Los predicados agrupan términos y tienen valor de verdad (verdadero o falso), como "le ha dado regalo a Juan" o "María le dio regalo a Juan" [24:09-24:35].

Predicados, conectivos y cuantificadores [24:35-25:23]

Los predicados expresan relaciones entre objetos ("se puede decir algo de alguien") [24:35-24:51]. Se repasan los conectivos `y`, `o` (∧, ∨), la negación (¬) y la implicación (→): "si A, entonces B" equivale a "o bien B, sólo si A"; también se menciona la doble implicación (↔) [24:51-25:23]. Se mencionan además los cuantificadores (∃, ∀) [25:05-25:13]. [parte no entendida — fragmentos sobre implicación y bicondicional].

Fórmulas, fórmula atómica, literal y prioridad de conectivos [25:23-27:00]

Una fórmula es un predicado o una combinación de fórmulas relacionadas por conectivos; los predicados son fórmulas y las combinaciones también, cada vez más elaboradas [25:53-26:23]. Se menciona la prioridad de los operadores (la negación es la de mayor prioridad) [26:33-26:41]. Una fórmula atómica es una fórmula que no contiene conectivos (un predicado "solito", p. ej. p(x)) [26:41-26:54]; una literal es una fórmula atómica o su negación [26:54-27:00].

La cláusula y las cláusulas de Horn [27:00-28:23]

Una cláusula es un tipo especial de fórmula: una disyunción de literales cuantificada universalmente (todas las variables "para todo") [27:00-28:03]. Dentro de las cláusulas hay un subconjunto destacado, las cláusulas de Horn, que tienen a lo sumo una literal no negada [28:11-28:23]. Son las cláusulas con las que se va a programar [28:23]. [parte no entendida — parte de la analogía para explicar la disyunción de literales].

La resolución restringida a cláusulas de Horn [28:23-29:47]

La explosión combinatoria es el gran inconveniente del método cuando se admiten cláusulas arbitrarias; por eso se restringe a un subconjunto (las cláusulas de Horn), con las cuales se va a programar [28:23-29:47]. Se comenta que no cualquier fórmula puede escribirse en esa forma ("que otros no se pueden poner aquí") y se muestra la forma de negar una disyunción para reescribirla [29:25-29:47].

Reglas, metas y negación de la meta [40:00-42:26]

Se trabaja con un conjunto de afirmaciones (las reglas y los hechos) y una meta que se quiere demostrar [41:24-42:26]. Las variables de las reglas se cuantifican universalmente ("para todo") [41:08-41:16]. Fijadas las reglas y aplicada la resolución, se busca deducir la meta para ver si la conclusión se sigue del conjunto [41:44-42:26]. [parte no entendida — tramo entre 29:47 y 40:00].

La contradicción y la cláusula vacía [42:26-44:00]

Para demostrar una meta A se la niega (¬A) y se la agrega al conjunto; si ese conjunto es verdadero y además se agrega ¬A, se llega a una contradicción [42:26-43:39]. La cláusula vacía (sin literales) es una contradicción: afirmar algo y su negación a la vez no puede ser cierto [43:23-44:00]. Si se llega a la contradicción, la meta se sigue de las premisas [43:31-44:00].

El resolvente y la demostración por resolución [47:55-49:58]

Al aplicar la resolución a dos cláusulas, el resultado se llama resolvente: lo que queda al cancelar los literales opuestos [47:55-48:56]. El resolvente tiene forma de nueva meta (nuevo objetivo) y se sigue aplicando la resolución entre cláusulas y resolventes [48:56-49:11]. Cuando se llega a la cláusula vacía, la demostración se ha completado [49:04-49:23]. Una demostración por resolución es una secuencia finita de resolventes, cada uno obtenido del anterior aplicando la resolución, hasta la cláusula vacía [49:13-49:58].

Ejemplo de demostración por resolución [60:00-62:43]

Se plantea una demostración a partir de un conjunto de reglas (cláusulas) y una meta, buscando la refutación del conjunto (llegar a la cláusula vacía) [60:00-60:25]. Se trabaja con cláusulas tipo A, B, C, A ∨ B, B ∨ C, etc., y se ve cómo combinarlas hasta obtener la contradicción [61:35-62:43]. [parte no entendida — gran parte del ejemplo; audio muy ruidoso].

Primer programa en Prolog: Proposiciones.pl, hechos, reglas y metas [62:43-65:34]

Se comienza a escribir el programa Proposiciones.pl para llevar la teoría a la práctica (se menciona la extensión .pl y los comentarios) [62:43-63:33]. Se distinguen los hechos (siempre verdaderos, sin condiciones) de las reglas, y se plantea una meta para consultar si algo es cierto [63:33-64:32]. La lógica proposicional queda limitada ("en proposiciones yo no puedo decir mucho"); el paso siguiente es usar variables para programar cosas más generales, que se continúa en la segunda parte [65:06-65:34]. [parte no entendida — fragmentos alrededor de la explicación del archivo y de las reglas].

2 Puntos destacados / Lo que hay que saber

3 Actividades y tareas pendientes

4 Dudas que podríamos tener

5 Sitios o recursos para visitar

6 Glosario de términos

• Resolvente: resultado de aplicar la resolución a dos cláusulas; la suma de sus literales menos los cancelados.
• Resolución: regla de inferencia para la demostración automática en lógica de primer orden.
• Demostración por resolución: secuencia finita de resolventes que termina en la cláusula vacía.
• Cláusula vacía (□): cláusula sin literales; es una contradicción e indica que la meta se sigue de las premisas.
• Cláusula: disyunción de literales cuantificada universalmente.
• Cláusula de Horn: cláusula con a lo sumo una literal no negada; base de Prolog.
• Fórmula atómica: fórmula sin conectivos (un predicado solo).
• Literal: una fórmula atómica o su negación.
• Término: una constante, una variable o una función con sus argumentos.
• Constante: nombre de un objeto o persona (p. ej. Juan, María).
• Variable: nombre que empieza con mayúscula (X) y puede tomar cualquier objeto o persona.
• Función: asociación de un nombre a sus argumentos constantes que devuelve un valor.
• Predicado: expresión que agrupa términos y tiene valor de verdad (verdadero o falso).
• Conectivos: y, o, la negación no y la implicación (∧, ∨, ¬, →, ↔).
• Cuantificadores: ∃ (existe) y ∀ (para todo).
• Explosión combinatoria: crecimiento desmesurado de las combinaciones a probar en la resolución; se reduce con las cláusulas de Horn.
• Prolog: lenguaje representativo de la programación lógica, basado en cláusulas de Horn.
• Hecho: cláusula siempre verdadera, sin condiciones, en Prolog.
• Regla: cláusula que establece una conclusión a partir de condiciones.
• Meta: objetivo que se quiere demostrar consultando el programa.
• Modus ponens: regla de inferencia: si Q implica P y Q, entonces P.

7 Mapa mental textual

• Resolución lógica y cláusulas: el resolvente y primeros programas en Prolog · Clase 10
  • Repaso de la resolución
    • Regla de Robinson / modus ponens
    • Demostración automática de la validez de fórmulas
    • Inconveniente: explosión combinatoria
  • Elementos del lenguaje (lógica de primer orden)
    • Constantes · variables (mayúscula) · funciones · términos
    • Predicados con valor de verdad
    • Conectivos ∧ ∨ ¬ → ↔ · cuantificadores ∃ ∀
    • Fórmula atómica (sin conectivos) · literal (atómica o su negación)
  • Cláusulas
    • Cláusula = disyunción de literales cuantificada universalmente
    • Cláusulas de Horn = a lo sumo una literal no negada
    • Restricción a Horn → reduce la explosión combinatoria
  • Demostración por resolución
    • Negar la meta y agregarla al conjunto
    • Resolvente = suma de literales menos los cancelados
    • Secuencia finita de resolventes → cláusula vacía (contradicción)
  • Primeros programas en Prolog
    • Proposiciones.pl · hechos · reglas · metas
    • Paso a usar variables (segunda parte)
    • Examen en equipos de dos